; EXPECT: unsat
;; slow conversion
; DISABLE-TESTER: alethe
(set-logic QF_UFLIRA)
(declare-sort FArray 2)


;-------------------------------------------------------------------------------
; Constants :
;-------------------------------------------------------------------------------



;-------------------------------------------------------------------------------
; State variables :
;-------------------------------------------------------------------------------

(declare-fun top.usr.onOff (Int) Bool)
(declare-fun top.usr.decelSet (Int) Bool)
(declare-fun top.usr.accelResume (Int) Bool)
(declare-fun top.usr.cancel (Int) Bool)
(declare-fun top.usr.brakePedal (Int) Bool)
(declare-fun top.usr.carGear (Int) Int)
(declare-fun top.usr.carSpeed (Int) Real)
(declare-fun top.usr.validInputs (Int) Bool)
(declare-fun top.usr.OK (Int) Bool)
(declare-fun top.res.init_flag (Int) Bool)
(declare-fun top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ (Int) Bool)
(declare-fun top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep (Int) Bool)
(declare-fun top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root (Int) Int)
(declare-fun top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out (Int) Int)
(declare-fun top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out (Int) Int)
(declare-fun top.res.subrange_1 (Int) Bool)
(declare-fun top.res.subrange_2 (Int) Bool)
(declare-fun top.res.subrange_3 (Int) Bool)
(declare-fun top.res.subrange_4 (Int) Bool)
(declare-fun top.res.subrange_5 (Int) Bool)
(set-info :system "Logical transition system generated by Kind2")
(set-info :input "sandbox/cruise_controller_01.lus")



;-------------------------------------------------------------------------------
; Function symbols :
;-------------------------------------------------------------------------------

(define-fun __node_init_top_0
 ((top.usr.onOff@0 Bool)
  (top.usr.decelSet@0 Bool)
  (top.usr.accelResume@0 Bool)
  (top.usr.cancel@0 Bool)
  (top.usr.brakePedal@0 Bool)
  (top.usr.carGear@0 Int)
  (top.usr.carSpeed@0 Real)
  (top.usr.validInputs@0 Bool)
  (top.usr.OK@0 Bool)
  (top.res.init_flag@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int)
  (top.res.subrange_1@0 Bool)
  (top.res.subrange_2@0 Bool)
  (top.res.subrange_3@0 Bool)
  (top.res.subrange_4@0 Bool)
  (top.res.subrange_5@0 Bool)) Bool
 (let
  ((X1 false))
  (let
   ((X2
     (and
      (and
       (and (and (not top.usr.cancel@0) (not top.usr.brakePedal@0)) (ite (= top.usr.carGear@0 3) true false))
       (ite (>= top.usr.carSpeed@0 15.0) true false))
      top.usr.validInputs@0)))
   (let
    ((X3 false))
    (let
     ((X4 0))
     (let
      ((X5 (ite (not top.usr.onOff@0) 0 1)))
      (let
       ((X6 (and (and (>= X4 2) (<= X4 8)) (not (ite (not (= X5 0)) true false)))))
       (let
        ((X7 (ite X6 (ite (and (>= X4 2) (<= X4 8)) 0 X4) X4)))
        (let
         ((X8 (ite X6 (ite (not (= X7 1)) 1 X7) X7)))
         (let
          ((X9 (and (= X8 1) (and (ite (not (= X5 0)) true false) (not X6)))))
          (let
           ((X10 (ite X9 (ite (= X8 1) 0 X8) X8)))
           (let
            ((X11 (ite (not (and (>= X10 2) (<= X10 8))) 2 X10)))
            (let
             ((X12 (and (not (and (>= X10 2) (<= X10 8))) (and (>= X11 2) (<= X11 8)))))
             (let
              ((X13 (ite X12 (ite (not (= X11 7)) 7 X11) X11)))
              (let
               ((X14 (ite X9 X13 X10)))
               (let
                ((X15 (ite (not X2) 0 1)))
                (let
                 ((X16 (and (and (>= X14 3) (<= X14 6)) (not (ite (not (= X15 0)) true false)))))
                 (let
                  ((X17 (ite X16 (ite (and (>= X14 3) (<= X14 6)) 2 X14) X14)))
                  (let
                   ((X18 (ite X16 (ite (not (= X17 8)) 8 X17) X17)))
                   (let
                    ((X19 (ite (not X1) 0 1)))
                    (let
                     ((X20
                       (and
                        (= X18 8)
                        (and
                         (and
                          (ite (not (= (ite (not (= X19 1)) 0 1) 0)) true false)
                          (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                         (not X16)))))
                     (let
                      ((X21 (ite X20 (ite (= X18 8) 2 X18) X18)))
                      (let
                       ((X22 (ite (not (and (>= X21 3) (<= X21 6))) 3 X21)))
                       (let
                        ((X23 (and (not (and (>= X21 3) (<= X21 6))) (and (>= X22 3) (<= X22 6)))))
                        (let
                         ((X24 (ite X23 (ite (not (= X22 4)) 4 X22) X22)))
                         (let
                          ((X25 (ite X20 X24 X21)))
                          (let
                           ((X26 (or X20 X16)))
                           (let
                            ((X27
                              (and
                               (= X25 8)
                               (and
                                (and
                                 (ite (not (= (ite (not (= (ite (not X3) 0 1) 1)) 0 1) 0)) true false)
                                 (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                                (not X26)))))
                            (let
                             ((X28 (ite X27 (ite (= X25 8) 2 X25) X25)))
                             (let
                              ((X29 (ite (not (and (>= X28 3) (<= X28 6))) 3 X28)))
                              (let
                               ((X30 (and (not (and (>= X28 3) (<= X28 6))) (and (>= X29 3) (<= X29 6)))))
                               (let
                                ((X31 (ite X30 (ite (not (= X29 4)) 4 X29) X29)))
                                (let
                                 ((X32 (ite X27 X31 X28)))
                                 (let
                                  ((X33 (or X27 X26)))
                                  (let
                                   ((X34
                                     (and
                                      (= X32 7)
                                      (and
                                       (and
                                        (ite (not (= (ite (not (= X19 1)) 0 1) 0)) true false)
                                        (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                                       (not X33)))))
                                   (let
                                    ((X35 (ite X34 (ite (= X32 7) 2 X32) X32)))
                                    (let
                                     ((X36 (ite (not (and (>= X35 3) (<= X35 6))) 3 X35)))
                                     (let
                                      ((X37 (and (not (and (>= X35 3) (<= X35 6))) (and (>= X36 3) (<= X36 6)))))
                                      (let
                                       ((X38 (ite X37 (ite (not (= X36 4)) 4 X36) X36)))
                                       (let
                                        ((X39 (or (= X38 4) (or (= X38 5) (= X38 6)))))
                                        (let
                                         ((X40 (ite (not (= X4 1)) 1 X4)))
                                         (let
                                          ((X41 (or X9 X6)))
                                          (let
                                           ((X42 (ite X34 X38 X35)))
                                           (let
                                            ((X43 (or X34 X33)))
                                            (let
                                             ((X44 (and (= X42 4) (= X19 1))))
                                             (let
                                              ((X45 (ite X44 (ite (= X42 4) 3 X42) X42)))
                                              (let
                                               ((X46 (ite X44 (ite (not (= X45 4)) 4 X45) X45)))
                                               (let
                                                ((X47
                                                  (ite
                                                   (not
                                                    (ite
                                                     (=
                                                      top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                      20)
                                                     true
                                                     false))
                                                   0
                                                   1)))
                                                (let
                                                 ((X48 (and (= X46 4) (and (= X47 1) (not X44)))))
                                                 (let
                                                  ((X49 (ite X48 (ite (= X46 4) 3 X46) X46)))
                                                  (let
                                                   ((X50 (ite X48 (ite (not (= X49 5)) 5 X49) X49)))
                                                   (let
                                                    ((X51 (or X48 X44)))
                                                    (let
                                                     ((X52
                                                       (ite
                                                        (not
                                                         (ite
                                                          (=
                                                           top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                           20)
                                                          true
                                                          false))
                                                        0
                                                        1)))
                                                     (let
                                                      ((X53 (and (= X50 4) (and (= X52 1) (not X51)))))
                                                      (let
                                                       ((X54 (ite X53 (ite (= X50 4) 3 X50) X50)))
                                                       (let
                                                        ((X55 (ite X53 (ite (not (= X54 6)) 6 X54) X54)))
                                                        (let
                                                         ((X56 (or X53 X51)))
                                                         (let
                                                          ((X57 (and (= X55 6) (and (= X52 0) (not X56)))))
                                                          (let
                                                           ((X58 (ite X57 (ite (= X55 6) 3 X55) X55)))
                                                           (let
                                                            ((X59 (ite X57 (ite (not (= X58 4)) 4 X58) X58)))
                                                            (let
                                                             ((X60 (or X57 X56)))
                                                             (let
                                                              ((X61 (and (= X59 5) (and (= X47 0) (not X60)))))
                                                              (let
                                                               ((X62 (ite X61 (ite (= X59 5) 3 X59) X59)))
                                                               (let
                                                                ((X63 (ite X61 (ite (not (= X62 4)) 4 X62) X62)))
                                                                (and
                                                                 (= top.usr.OK@0 X39)
                                                                 (=
                                                                  top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                                  (ite
                                                                   (<=
                                                                    (ite
                                                                    (>= 0 (ite top.usr.decelSet@0 1 0))
                                                                    0
                                                                    (ite top.usr.decelSet@0 1 0))
                                                                    20)
                                                                   (ite
                                                                    (>= 0 (ite top.usr.decelSet@0 1 0))
                                                                    0
                                                                    (ite top.usr.decelSet@0 1 0))
                                                                   20))
                                                                 (=
                                                                  top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                                  (ite
                                                                   (<=
                                                                    (ite
                                                                    (>= 0 (ite top.usr.accelResume@0 1 0))
                                                                    0
                                                                    (ite top.usr.accelResume@0 1 0))
                                                                    20)
                                                                   (ite
                                                                    (>= 0 (ite top.usr.accelResume@0 1 0))
                                                                    0
                                                                    (ite top.usr.accelResume@0 1 0))
                                                                   20))
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0
                                                                  true)
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0
                                                                  true)
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0
                                                                  (ite
                                                                   top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0
                                                                   (ite
                                                                    top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0
                                                                    X40
                                                                    (ite
                                                                    (and (not X41) (and (>= X14 2) (<= X14 8)))
                                                                    (ite
                                                                    (and (not X43) (and (>= X42 3) (<= X42 6)))
                                                                    X63
                                                                    X42)
                                                                    X14))
                                                                   X4))
                                                                 (= top.res.subrange_1@0 (and (<= 0 X5) (<= X5 1)))
                                                                 (= top.res.subrange_2@0 (and (<= 0 X52) (<= X52 1)))
                                                                 (= top.res.subrange_3@0 (and (<= 0 X19) (<= X19 1)))
                                                                 (= top.res.subrange_4@0 (and (<= 0 X47) (<= X47 1)))
                                                                 (= top.res.subrange_5@0 (and (<= 0 X15) (<= X15 1)))
                                                                 top.res.init_flag@0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(define-fun __node_trans_top_0
 ((top.usr.onOff@1 Bool)
  (top.usr.decelSet@1 Bool)
  (top.usr.accelResume@1 Bool)
  (top.usr.cancel@1 Bool)
  (top.usr.brakePedal@1 Bool)
  (top.usr.carGear@1 Int)
  (top.usr.carSpeed@1 Real)
  (top.usr.validInputs@1 Bool)
  (top.usr.OK@1 Bool)
  (top.res.init_flag@1 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1 Int)
  (top.res.subrange_1@1 Bool)
  (top.res.subrange_2@1 Bool)
  (top.res.subrange_3@1 Bool)
  (top.res.subrange_4@1 Bool)
  (top.res.subrange_5@1 Bool)
  (top.usr.onOff@0 Bool)
  (top.usr.decelSet@0 Bool)
  (top.usr.accelResume@0 Bool)
  (top.usr.cancel@0 Bool)
  (top.usr.brakePedal@0 Bool)
  (top.usr.carGear@0 Int)
  (top.usr.carSpeed@0 Real)
  (top.usr.validInputs@0 Bool)
  (top.usr.OK@0 Bool)
  (top.res.init_flag@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0 Bool)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0 Int)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0 Int)
  (top.res.subrange_1@0 Bool)
  (top.res.subrange_2@0 Bool)
  (top.res.subrange_3@0 Bool)
  (top.res.subrange_4@0 Bool)
  (top.res.subrange_5@0 Bool)) Bool
 (let
  ((X1 (and (not top.usr.decelSet@0) top.usr.decelSet@1)))
  (let
   ((X2
     (and
      (and
       (and (and (not top.usr.cancel@1) (not top.usr.brakePedal@1)) (ite (= top.usr.carGear@1 3) true false))
       (ite (>= top.usr.carSpeed@1 15.0) true false))
      top.usr.validInputs@1)))
   (let
    ((X3 (and (not top.usr.accelResume@0) top.usr.accelResume@1)))
    (let
     ((X4 top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@0))
     (let
      ((X5 (ite (not top.usr.onOff@1) 0 1)))
      (let
       ((X6 (and (and (>= X4 2) (<= X4 8)) (not (ite (not (= X5 0)) true false)))))
       (let
        ((X7 (ite X6 (ite (and (>= X4 2) (<= X4 8)) 0 X4) X4)))
        (let
         ((X8 (ite X6 (ite (not (= X7 1)) 1 X7) X7)))
         (let
          ((X9 (and (= X8 1) (and (ite (not (= X5 0)) true false) (not X6)))))
          (let
           ((X10 (ite X9 (ite (= X8 1) 0 X8) X8)))
           (let
            ((X11 (ite (not (and (>= X10 2) (<= X10 8))) 2 X10)))
            (let
             ((X12 (and (not (and (>= X10 2) (<= X10 8))) (and (>= X11 2) (<= X11 8)))))
             (let
              ((X13 (ite X12 (ite (not (= X11 7)) 7 X11) X11)))
              (let
               ((X14 (ite X9 X13 X10)))
               (let
                ((X15 (ite (not X2) 0 1)))
                (let
                 ((X16 (and (and (>= X14 3) (<= X14 6)) (not (ite (not (= X15 0)) true false)))))
                 (let
                  ((X17 (ite X16 (ite (and (>= X14 3) (<= X14 6)) 2 X14) X14)))
                  (let
                   ((X18 (ite X16 (ite (not (= X17 8)) 8 X17) X17)))
                   (let
                    ((X19 (ite (not X1) 0 1)))
                    (let
                     ((X20
                       (and
                        (= X18 8)
                        (and
                         (and
                          (ite (not (= (ite (not (= X19 1)) 0 1) 0)) true false)
                          (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                         (not X16)))))
                     (let
                      ((X21 (ite X20 (ite (= X18 8) 2 X18) X18)))
                      (let
                       ((X22 (ite (not (and (>= X21 3) (<= X21 6))) 3 X21)))
                       (let
                        ((X23 (and (not (and (>= X21 3) (<= X21 6))) (and (>= X22 3) (<= X22 6)))))
                        (let
                         ((X24 (ite X23 (ite (not (= X22 4)) 4 X22) X22)))
                         (let
                          ((X25 (ite X20 X24 X21)))
                          (let
                           ((X26 (or X20 X16)))
                           (let
                            ((X27
                              (and
                               (= X25 8)
                               (and
                                (and
                                 (ite (not (= (ite (not (= (ite (not X3) 0 1) 1)) 0 1) 0)) true false)
                                 (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                                (not X26)))))
                            (let
                             ((X28 (ite X27 (ite (= X25 8) 2 X25) X25)))
                             (let
                              ((X29 (ite (not (and (>= X28 3) (<= X28 6))) 3 X28)))
                              (let
                               ((X30 (and (not (and (>= X28 3) (<= X28 6))) (and (>= X29 3) (<= X29 6)))))
                               (let
                                ((X31 (ite X30 (ite (not (= X29 4)) 4 X29) X29)))
                                (let
                                 ((X32 (ite X27 X31 X28)))
                                 (let
                                  ((X33 (or X27 X26)))
                                  (let
                                   ((X34
                                     (and
                                      (= X32 7)
                                      (and
                                       (and
                                        (ite (not (= (ite (not (= X19 1)) 0 1) 0)) true false)
                                        (ite (not (= (ite (not (= X15 1)) 0 1) 0)) true false))
                                       (not X33)))))
                                   (let
                                    ((X35 (ite X34 (ite (= X32 7) 2 X32) X32)))
                                    (let
                                     ((X36 (ite (not (and (>= X35 3) (<= X35 6))) 3 X35)))
                                     (let
                                      ((X37 (and (not (and (>= X35 3) (<= X35 6))) (and (>= X36 3) (<= X36 6)))))
                                      (let
                                       ((X38 (ite X37 (ite (not (= X36 4)) 4 X36) X36)))
                                       (let
                                        ((X39 (or (= X38 4) (or (= X38 5) (= X38 6)))))
                                        (let
                                         ((X40 (ite (not (= X4 1)) 1 X4)))
                                         (let
                                          ((X41 (or X9 X6)))
                                          (let
                                           ((X42 (ite X34 X38 X35)))
                                           (let
                                            ((X43 (or X34 X33)))
                                            (let
                                             ((X44 (and (= X42 4) (= X19 1))))
                                             (let
                                              ((X45 (ite X44 (ite (= X42 4) 3 X42) X42)))
                                              (let
                                               ((X46 (ite X44 (ite (not (= X45 4)) 4 X45) X45)))
                                               (let
                                                ((X47
                                                  (ite
                                                   (not
                                                    (ite
                                                     (=
                                                      top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1
                                                      20)
                                                     true
                                                     false))
                                                   0
                                                   1)))
                                                (let
                                                 ((X48 (and (= X46 4) (and (= X47 1) (not X44)))))
                                                 (let
                                                  ((X49 (ite X48 (ite (= X46 4) 3 X46) X46)))
                                                  (let
                                                   ((X50 (ite X48 (ite (not (= X49 5)) 5 X49) X49)))
                                                   (let
                                                    ((X51 (or X48 X44)))
                                                    (let
                                                     ((X52
                                                       (ite
                                                        (not
                                                         (ite
                                                          (=
                                                           top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1
                                                           20)
                                                          true
                                                          false))
                                                        0
                                                        1)))
                                                     (let
                                                      ((X53 (and (= X50 4) (and (= X52 1) (not X51)))))
                                                      (let
                                                       ((X54 (ite X53 (ite (= X50 4) 3 X50) X50)))
                                                       (let
                                                        ((X55 (ite X53 (ite (not (= X54 6)) 6 X54) X54)))
                                                        (let
                                                         ((X56 (or X53 X51)))
                                                         (let
                                                          ((X57 (and (= X55 6) (and (= X52 0) (not X56)))))
                                                          (let
                                                           ((X58 (ite X57 (ite (= X55 6) 3 X55) X55)))
                                                           (let
                                                            ((X59 (ite X57 (ite (not (= X58 4)) 4 X58) X58)))
                                                            (let
                                                             ((X60 (or X57 X56)))
                                                             (let
                                                              ((X61 (and (= X59 5) (and (= X47 0) (not X60)))))
                                                              (let
                                                               ((X62 (ite X61 (ite (= X59 5) 3 X59) X59)))
                                                               (let
                                                                ((X63 (ite X61 (ite (not (= X62 4)) 4 X62) X62)))
                                                                (and
                                                                 (= top.usr.OK@1 X39)
                                                                 (=
                                                                  top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@1
                                                                  (ite
                                                                   (<=
                                                                    (ite
                                                                    (>=
                                                                    0
                                                                    (ite
                                                                    top.usr.decelSet@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    0
                                                                    (ite
                                                                    top.usr.decelSet@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    20)
                                                                   (ite
                                                                    (>=
                                                                    0
                                                                    (ite
                                                                    top.usr.decelSet@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    0
                                                                    (ite
                                                                    top.usr.decelSet@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                   20))
                                                                 (=
                                                                  top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@1
                                                                  (ite
                                                                   (<=
                                                                    (ite
                                                                    (>=
                                                                    0
                                                                    (ite
                                                                    top.usr.accelResume@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    0
                                                                    (ite
                                                                    top.usr.accelResume@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    20)
                                                                   (ite
                                                                    (>=
                                                                    0
                                                                    (ite
                                                                    top.usr.accelResume@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                    0
                                                                    (ite
                                                                    top.usr.accelResume@1
                                                                    (+
                                                                    top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out@0
                                                                    1)
                                                                    0))
                                                                   20))
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1
                                                                  (ite
                                                                   top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@0
                                                                   false
                                                                   top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@0))
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1
                                                                  true)
                                                                 (=
                                                                  top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root@1
                                                                  (ite
                                                                   top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___@1
                                                                   (ite
                                                                    top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep@1
                                                                    X40
                                                                    (ite
                                                                    (and (not X41) (and (>= X14 2) (<= X14 8)))
                                                                    (ite
                                                                    (and (not X43) (and (>= X42 3) (<= X42 6)))
                                                                    X63
                                                                    X42)
                                                                    X14))
                                                                   X4))
                                                                 (= top.res.subrange_1@1 (and (<= 0 X5) (<= X5 1)))
                                                                 (= top.res.subrange_2@1 (and (<= 0 X52) (<= X52 1)))
                                                                 (= top.res.subrange_3@1 (and (<= 0 X19) (<= X19 1)))
                                                                 (= top.res.subrange_4@1 (and (<= 0 X47) (<= X47 1)))
                                                                 (= top.res.subrange_5@1 (and (<= 0 X15) (<= X15 1)))
                                                                 (not top.res.init_flag@1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))



;-------------------------------------------------------------------------------
; Initial states :
;-------------------------------------------------------------------------------

(define-fun I1 ((i Int)) Bool
 (__node_init_top_0
  (top.usr.onOff i)
  (top.usr.decelSet i)
  (top.usr.accelResume i)
  (top.usr.cancel i)
  (top.usr.brakePedal i)
  (top.usr.carGear i)
  (top.usr.carSpeed i)
  (top.usr.validInputs i)
  (top.usr.OK i)
  (top.res.init_flag i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root i)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out i)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out i)
  (top.res.subrange_1 i)
  (top.res.subrange_2 i)
  (top.res.subrange_3 i)
  (top.res.subrange_4 i)
  (top.res.subrange_5 i)))



;-------------------------------------------------------------------------------
; Transition_relation :
;-------------------------------------------------------------------------------

(define-fun T1 ((i Int) (j Int)) Bool
 (__node_trans_top_0
  (top.usr.onOff j)
  (top.usr.decelSet j)
  (top.usr.accelResume j)
  (top.usr.cancel j)
  (top.usr.brakePedal j)
  (top.usr.carGear j)
  (top.usr.carSpeed j)
  (top.usr.validInputs j)
  (top.usr.OK j)
  (top.res.init_flag j)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ j)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep j)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root j)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out j)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out j)
  (top.res.subrange_1 j)
  (top.res.subrange_2 j)
  (top.res.subrange_3 j)
  (top.res.subrange_4 j)
  (top.res.subrange_5 j)
  (top.usr.onOff i)
  (top.usr.decelSet i)
  (top.usr.accelResume i)
  (top.usr.cancel i)
  (top.usr.brakePedal i)
  (top.usr.carGear i)
  (top.usr.carSpeed i)
  (top.usr.validInputs i)
  (top.usr.OK i)
  (top.res.init_flag i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic____wakeup___ i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_rlt_evtInitStep i)
  (top.impl.usr.chart_CruiseController_ModeLogic_mode_logic_final_state_states___root i)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetAccel_Bounded_Count_Out i)
  (top.impl.usr.cruise_controller_CruiseController_ModeLogic_DelayOnsetDecel_Bounded_Count_Out i)
  (top.res.subrange_1 i)
  (top.res.subrange_2 i)
  (top.res.subrange_3 i)
  (top.res.subrange_4 i)
  (top.res.subrange_5 i)))



;-------------------------------------------------------------------------------
; Original property :
;-------------------------------------------------------------------------------

(define-fun P1 ((i Int)) Bool (top.usr.OK i))



;-------------------------------------------------------------------------------
; k-Inductive invariant :
;-------------------------------------------------------------------------------

(define-fun PHI1 ((i Int)) Bool (top.usr.OK i))



;-------------------------------------------------------------------------------
; Base case :
;-------------------------------------------------------------------------------

(assert (or (and (I1 0) (not (PHI1 0))) (and (and (I1 0) (T1 0 1)) (not (PHI1 1)))))

(check-sat)
(exit)
